k:Knd. k = k ~ tt 

latex

Definitions	b, t  T, x:A. B(x), a = b, P  Q, P  Q, P & Q, P  Q, Knd, , {T}, SQType(T), KindDeq
Lemmas	deq property, Kind-deq wf, bool sq, Knd wf, eqtt to assert, eq knd wf